(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 1))
(let ((e3 1))
(let ((e4 0))
(let ((e5 (- v1)))
(let ((e6 (+ e5 e5)))
(let ((e7 (- e6 v1)))
(let ((e8 (/ e4 (- e3))))
(let ((e9 (+ e8 v1)))
(let ((e10 (* v1 (- e3))))
(let ((e11 (* (- e2) e5)))
(let ((e12 (* e4 e5)))
(let ((e13 (- v0)))
(let ((e14 (distinct e13 e12)))
(let ((e15 (>= e7 e9)))
(let ((e16 (distinct e6 e9)))
(let ((e17 (> e6 e8)))
(let ((e18 (= e10 v1)))
(let ((e19 (= e11 e9)))
(let ((e20 (<= e9 e12)))
(let ((e21 (distinct e7 e5)))
(let ((e22 (> e9 e6)))
(let ((e23 (< e12 e5)))
(let ((e24 (= e6 e9)))
(let ((e25 (<= e8 e6)))
(let ((e26 (distinct e8 e12)))
(let ((e27 (distinct v1 e9)))
(let ((e28 (distinct e9 e10)))
(let ((e29 (< e10 e10)))
(let ((e30 (> e13 v0)))
(let ((e31 (ite e23 v0 v0)))
(let ((e32 (ite e27 e12 e31)))
(let ((e33 (ite e19 v1 e8)))
(let ((e34 (ite e28 e13 e32)))
(let ((e35 (ite e22 e32 v1)))
(let ((e36 (ite e17 e6 e5)))
(let ((e37 (ite e16 e31 e10)))
(let ((e38 (ite e21 e31 e32)))
(let ((e39 (ite e24 e9 e32)))
(let ((e40 (ite e15 e12 e35)))
(let ((e41 (ite e15 e13 e36)))
(let ((e42 (ite e29 e7 e7)))
(let ((e43 (ite e21 e5 e10)))
(let ((e44 (ite e26 e5 e43)))
(let ((e45 (ite e30 e11 e13)))
(let ((e46 (ite e26 e11 e6)))
(let ((e47 (ite e20 e45 e33)))
(let ((e48 (ite e23 e44 e34)))
(let ((e49 (ite e23 e41 e42)))
(let ((e50 (ite e14 e34 e10)))
(let ((e51 (ite e16 e35 e35)))
(let ((e52 (ite e30 e34 e49)))
(let ((e53 (ite e28 e43 e50)))
(let ((e54 (ite e14 e51 e52)))
(let ((e55 (ite e18 e53 e5)))
(let ((e56 (ite e25 e36 e34)))
(let ((e57 (<= e44 e40)))
(let ((e58 (= e47 e41)))
(let ((e59 (< e52 e10)))
(let ((e60 (<= e50 e8)))
(let ((e61 (distinct e33 e41)))
(let ((e62 (= e46 e55)))
(let ((e63 (>= e46 e8)))
(let ((e64 (< e52 e47)))
(let ((e65 (= e13 e5)))
(let ((e66 (< e40 e32)))
(let ((e67 (distinct e34 e55)))
(let ((e68 (<= e50 e56)))
(let ((e69 (<= e10 e32)))
(let ((e70 (< e55 e56)))
(let ((e71 (distinct e31 e56)))
(let ((e72 (> e53 v0)))
(let ((e73 (= e51 e7)))
(let ((e74 (distinct e37 e52)))
(let ((e75 (> e37 e9)))
(let ((e76 (>= e13 e42)))
(let ((e77 (>= e40 e6)))
(let ((e78 (< e38 e11)))
(let ((e79 (< e39 e38)))
(let ((e80 (> e51 e40)))
(let ((e81 (> v0 e32)))
(let ((e82 (> e6 e40)))
(let ((e83 (>= e48 e40)))
(let ((e84 (< e6 e31)))
(let ((e85 (> e12 e47)))
(let ((e86 (= e49 e49)))
(let ((e87 (distinct e12 e40)))
(let ((e88 (= e49 e51)))
(let ((e89 (>= v0 e56)))
(let ((e90 (>= e10 e47)))
(let ((e91 (> e9 e39)))
(let ((e92 (< e46 e40)))
(let ((e93 (distinct e55 e40)))
(let ((e94 (< e53 e13)))
(let ((e95 (= e47 v1)))
(let ((e96 (<= e46 e53)))
(let ((e97 (< e56 e46)))
(let ((e98 (>= e36 e45)))
(let ((e99 (< e49 e46)))
(let ((e100 (<= e56 e35)))
(let ((e101 (distinct e46 e45)))
(let ((e102 (> e6 e38)))
(let ((e103 (>= e11 e52)))
(let ((e104 (< e33 e45)))
(let ((e105 (> e7 e47)))
(let ((e106 (= e13 e51)))
(let ((e107 (< e40 v1)))
(let ((e108 (distinct e40 e47)))
(let ((e109 (>= e36 e53)))
(let ((e110 (> e40 e54)))
(let ((e111 (< e38 e12)))
(let ((e112 (<= e34 e51)))
(let ((e113 (<= e48 e11)))
(let ((e114 (> e7 e35)))
(let ((e115 (>= e44 e7)))
(let ((e116 (>= e42 e47)))
(let ((e117 (>= e56 e6)))
(let ((e118 (>= e54 e53)))
(let ((e119 (distinct e39 e40)))
(let ((e120 (= e33 e40)))
(let ((e121 (= e9 e52)))
(let ((e122 (<= v1 e41)))
(let ((e123 (< e49 e13)))
(let ((e124 (<= e31 e34)))
(let ((e125 (<= e52 e50)))
(let ((e126 (< e46 e37)))
(let ((e127 (<= e13 e12)))
(let ((e128 (< e31 e55)))
(let ((e129 (>= e39 e44)))
(let ((e130 (> e8 e37)))
(let ((e131 (> e33 e47)))
(let ((e132 (> e37 e51)))
(let ((e133 (= e50 e41)))
(let ((e134 (>= e10 e7)))
(let ((e135 (>= e50 e33)))
(let ((e136 (< e41 e52)))
(let ((e137 (distinct e56 e40)))
(let ((e138 (distinct e13 e47)))
(let ((e139 (< e41 e49)))
(let ((e140 (= e10 e45)))
(let ((e141 (= e37 e45)))
(let ((e142 (< e10 e40)))
(let ((e143 (<= e44 e39)))
(let ((e144 (>= e43 e33)))
(let ((e145 (= e107 e87)))
(let ((e146 (not e102)))
(let ((e147 (ite e127 e99 e89)))
(let ((e148 (not e117)))
(let ((e149 (not e72)))
(let ((e150 (ite e17 e141 e133)))
(let ((e151 (ite e135 e122 e137)))
(let ((e152 (= e134 e120)))
(let ((e153 (=> e68 e15)))
(let ((e154 (not e112)))
(let ((e155 (= e19 e123)))
(let ((e156 (xor e128 e64)))
(let ((e157 (not e85)))
(let ((e158 (=> e95 e71)))
(let ((e159 (or e115 e130)))
(let ((e160 (ite e108 e103 e101)))
(let ((e161 (or e110 e147)))
(let ((e162 (not e76)))
(let ((e163 (=> e155 e143)))
(let ((e164 (or e21 e149)))
(let ((e165 (ite e146 e24 e28)))
(let ((e166 (=> e91 e91)))
(let ((e167 (xor e160 e145)))
(let ((e168 (and e106 e111)))
(let ((e169 (=> e156 e167)))
(let ((e170 (not e164)))
(let ((e171 (=> e153 e90)))
(let ((e172 (not e73)))
(let ((e173 (=> e158 e16)))
(let ((e174 (not e157)))
(let ((e175 (or e131 e78)))
(let ((e176 (=> e144 e136)))
(let ((e177 (and e165 e139)))
(let ((e178 (not e126)))
(let ((e179 (xor e88 e59)))
(let ((e180 (xor e171 e121)))
(let ((e181 (= e100 e161)))
(let ((e182 (xor e151 e109)))
(let ((e183 (xor e129 e60)))
(let ((e184 (=> e25 e30)))
(let ((e185 (or e97 e179)))
(let ((e186 (ite e152 e138 e176)))
(let ((e187 (not e86)))
(let ((e188 (or e20 e150)))
(let ((e189 (=> e140 e174)))
(let ((e190 (= e65 e148)))
(let ((e191 (=> e92 e188)))
(let ((e192 (xor e70 e29)))
(let ((e193 (=> e168 e113)))
(let ((e194 (=> e181 e23)))
(let ((e195 (= e119 e84)))
(let ((e196 (= e190 e175)))
(let ((e197 (or e82 e124)))
(let ((e198 (= e183 e58)))
(let ((e199 (=> e105 e159)))
(let ((e200 (=> e80 e198)))
(let ((e201 (and e200 e189)))
(let ((e202 (or e57 e187)))
(let ((e203 (or e162 e178)))
(let ((e204 (ite e180 e163 e202)))
(let ((e205 (ite e182 e197 e197)))
(let ((e206 (= e18 e191)))
(let ((e207 (ite e62 e75 e125)))
(let ((e208 (= e207 e81)))
(let ((e209 (=> e74 e74)))
(let ((e210 (ite e79 e170 e205)))
(let ((e211 (ite e185 e201 e206)))
(let ((e212 (ite e69 e118 e196)))
(let ((e213 (and e96 e177)))
(let ((e214 (or e186 e169)))
(let ((e215 (not e210)))
(let ((e216 (= e173 e22)))
(let ((e217 (or e166 e98)))
(let ((e218 (=> e217 e217)))
(let ((e219 (ite e14 e94 e184)))
(let ((e220 (or e116 e213)))
(let ((e221 (ite e211 e132 e61)))
(let ((e222 (=> e218 e195)))
(let ((e223 (xor e208 e215)))
(let ((e224 (not e199)))
(let ((e225 (xor e93 e192)))
(let ((e226 (or e27 e223)))
(let ((e227 (ite e83 e66 e77)))
(let ((e228 (= e114 e204)))
(let ((e229 (xor e214 e67)))
(let ((e230 (ite e220 e229 e142)))
(let ((e231 (=> e154 e63)))
(let ((e232 (and e203 e209)))
(let ((e233 (=> e230 e225)))
(let ((e234 (and e194 e226)))
(let ((e235 (and e172 e233)))
(let ((e236 (xor e212 e26)))
(let ((e237 (xor e234 e235)))
(let ((e238 (and e216 e227)))
(let ((e239 (xor e221 e193)))
(let ((e240 (and e237 e237)))
(let ((e241 (ite e236 e238 e222)))
(let ((e242 (not e239)))
(let ((e243 (and e242 e240)))
(let ((e244 (and e243 e228)))
(let ((e245 (not e104)))
(let ((e246 (not e231)))
(let ((e247 (= e232 e232)))
(let ((e248 (and e219 e244)))
(let ((e249 (=> e241 e246)))
(let ((e250 (and e248 e245)))
(let ((e251 (ite e224 e249 e224)))
(let ((e252 (xor e250 e247)))
(let ((e253 (=> e252 e252)))
(let ((e254 (or e253 e253)))
(let ((e255 (and e251 e254)))
e255
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
